Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    rev(nil)  → nil
2:    rev(x ++ y)  → rev1(x,y) ++ rev2(x,y)
3:    rev1(x,nil)  → x
4:    rev1(x,y ++ z)  → rev1(y,z)
5:    rev2(x,nil)  → nil
6:    rev2(x,y ++ z)  → rev(x ++ rev(rev2(y,z)))
There are 6 dependency pairs:
7:    REV(x ++ y)  → REV1(x,y)
8:    REV(x ++ y)  → REV2(x,y)
9:    REV1(x,y ++ z)  → REV1(y,z)
10:    REV2(x,y ++ z)  → REV(x ++ rev(rev2(y,z)))
11:    REV2(x,y ++ z)  → REV(rev2(y,z))
12:    REV2(x,y ++ z)  → REV2(y,z)
The approximated dependency graph contains 2 SCCs: {9} and {8,10-12}.
Tyrolean Termination Tool  (0.12 seconds)   ---  May 4, 2006